$\forall$$A$,$B$:es\_realizer\{i:l\}. R{-}compat\{i:l\}($A$; $B$) $\in$ prop\{i':l\}